\begin{tabbing}
weak{-}send{-}do{-}apply(${\it es}$;$T$;$l$;${\it tg}$;$a$;${\it ds}$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$discrete{-}weak{-}precond{-}send{-}p(\=${\it es}$;$T$;\{0..1$^{-}$\};$l$;${\it tg}$;$a$;${\it ds}$;\+
\\[0ex]$\lambda$$s$.can{-}apply($f$;$s$);$\lambda$$s$,$v$. do{-}apply($f$;$s$))
\-
\end{tabbing}